Problem:
 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
 plus(N,0()) -> N
 plus(N,s(M)) -> U11(tt(),M,N)
 activate(X) -> X

Proof:
 Complexity Transformation Processor:
  strict:
   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
   plus(N,0()) -> N
   plus(N,s(M)) -> U11(tt(),M,N)
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 248,
     
     [s](x0) = x0 + 51,
     
     [plus](x0, x1) = x0 + x1 + 70,
     
     [U12](x0, x1, x2) = x0 + x1 + x2 + 236,
     
     [activate](x0) = x0 + 4,
     
     [U11](x0, x1, x2) = x0 + x1 + x2 + 120,
     
     [tt] = 148
    orientation:
     U11(tt(),M,N) = M + N + 268 >= M + N + 392 = U12(tt(),activate(M),activate(N))
     
     U12(tt(),M,N) = M + N + 384 >= M + N + 129 = s(plus(activate(N),activate(M)))
     
     plus(N,0()) = N + 318 >= N = N
     
     plus(N,s(M)) = M + N + 121 >= M + N + 268 = U11(tt(),M,N)
     
     activate(X) = X + 4 >= X = X
    problem:
     strict:
      U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
      plus(N,s(M)) -> U11(tt(),M,N)
     weak:
      U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
      plus(N,0()) -> N
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [0] = 0,
       
       [s](x0) = x0 + 3,
       
       [plus](x0, x1) = x0 + x1,
       
       [U12](x0, x1, x2) = x0 + x1 + x2 + 3,
       
       [activate](x0) = x0,
       
       [U11](x0, x1, x2) = x0 + x1 + x2 + 10,
       
       [tt] = 0
      orientation:
       U11(tt(),M,N) = M + N + 10 >= M + N + 3 = U12(tt(),activate(M),activate(N))
       
       plus(N,s(M)) = M + N + 3 >= M + N + 10 = U11(tt(),M,N)
       
       U12(tt(),M,N) = M + N + 3 >= M + N + 3 = s(plus(activate(N),activate(M)))
       
       plus(N,0()) = N >= N = N
       
       activate(X) = X >= X = X
      problem:
       strict:
        plus(N,s(M)) -> U11(tt(),M,N)
       weak:
        U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
        U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
        plus(N,0()) -> N
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 3]
        [0 1]
        interpretation:
               [1]
         [0] = [2],
         
                        [0]
         [s](x0) = x0 + [3],
         
                               [1 3]     [0]
         [plus](x0, x1) = x0 + [0 1]x1 + [2],
         
                             [1 2]     [1 3]          [0]
         [U12](x0, x1, x2) = [0 1]x0 + [0 1]x1 + x2 + [3],
         
                               [2]
         [activate](x0) = x0 + [0],
         
                             [1 3]     [1 3]          [2]
         [U11](x0, x1, x2) = [0 1]x0 + [0 1]x1 + x2 + [3],
         
                [0]
         [tt] = [2]
        orientation:
                        [1 3]        [9]    [1 3]        [8]                
         plus(N,s(M)) = [0 1]M + N + [5] >= [0 1]M + N + [5] = U11(tt(),M,N)
         
                         [1 3]        [8]    [1 3]        [8]                                    
         U11(tt(),M,N) = [0 1]M + N + [5] >= [0 1]M + N + [5] = U12(tt(),activate(M),activate(N))
         
                         [1 3]        [4]    [1 3]        [4]                                   
         U12(tt(),M,N) = [0 1]M + N + [5] >= [0 1]M + N + [5] = s(plus(activate(N),activate(M)))
         
                           [7]         
         plus(N,0()) = N + [4] >= N = N
         
                           [2]         
         activate(X) = X + [0] >= X = X
        problem:
         strict:
          
         weak:
          plus(N,s(M)) -> U11(tt(),M,N)
          U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
          U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
          plus(N,0()) -> N
          activate(X) -> X
        Qed